Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(lt,app(s,x)),app(s,y))  → app(app(lt,x),y)
2:    app(app(lt,0),app(s,y))  → true
3:    app(app(lt,y),0)  → false
4:    app(app(eq,x),x)  → true
5:    app(app(eq,app(s,x)),0)  → false
6:    app(app(eq,0),app(s,x))  → false
7:    app(app(member,w),null)  → false
8:    app(app(member,w),app(app(app(fork,x),y),z))  → app(app(app(if,app(app(lt,w),y)),app(app(member,w),x)),app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z)))
There are 14 dependency pairs:
9:    APP(app(lt,app(s,x)),app(s,y))  → APP(app(lt,x),y)
10:    APP(app(lt,app(s,x)),app(s,y))  → APP(lt,x)
11:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(app(if,app(app(lt,w),y)),app(app(member,w),x)),app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z)))
12:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(if,app(app(lt,w),y)),app(app(member,w),x))
13:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(if,app(app(lt,w),y))
14:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(lt,w),y)
15:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(lt,w)
16:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(member,w),x)
17:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z))
18:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(if,app(app(eq,w),y)),true)
19:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(if,app(app(eq,w),y))
20:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(eq,w),y)
21:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(eq,w)
22:    APP(app(member,w),app(app(app(fork,x),y),z))  → APP(app(member,w),z)
The approximated dependency graph contains one SCC: {9,11,12,14,16,17,20,22}.
Tyrolean Termination Tool  (36.31 seconds)   ---  May 3, 2006